<html>
<head><meta charset="utf-8"><title>Master&#x27;s Work · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html">Master&#x27;s Work</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="209486519"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209486519" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209486519">(Sep 09 2020 at 08:56)</a>:</h4>
<p>Hey, if anyone's interested, here's the report from my master's internship / final project. I developed a translation from a MIR-like language to a WhyML-like language and proved it correct. It uses the same representation of borrows shown in RustHorn as a pair of a current and 'final' value.</p>



<a name="209486522"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209486522" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209486522">(Sep 09 2020 at 08:56)</a>:</h4>
<p><a href="/user_uploads/4715/vVQNWxC9ZALl65oHkmB4Lrbr/paper.pdf">paper.pdf</a></p>



<a name="209486563"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209486563" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209486563">(Sep 09 2020 at 08:56)</a>:</h4>
<p>I'll be starting from this for my PhD thesis in october.</p>



<a name="209486630"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209486630" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209486630">(Sep 09 2020 at 08:57)</a>:</h4>
<p>There was a page limit of 18 pages on the report so if anyone has questions don't hesitate to ask.</p>



<a name="209549274"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209549274" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209549274">(Sep 09 2020 at 18:27)</a>:</h4>
<p>Do you know how this relates to Sebastian Ullrich's Electrolysis?<br>
(Electrolysis translated Rust to Lean so that you could verify the code. My memory was that it also used ideas from RustHorn - but I don't see any mention so I must be imagining it.)</p>
<p>Blog: <a href="https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html">https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html</a><br>
Masters thesis: <a href="https://pp.ipd.kit.edu/uploads/publikationen/ullrich16masterarbeit.pdf">https://pp.ipd.kit.edu/uploads/publikationen/ullrich16masterarbeit.pdf</a><br>
Slides: <a href="http://kha.github.io/electrolysis/presentation.pdf">http://kha.github.io/electrolysis/presentation.pdf</a><br>
Code: <a href="https://github.com/Kha/electrolysis">https://github.com/Kha/electrolysis</a> (no longer being developed)</p>



<a name="209561857"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209561857" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209561857">(Sep 09 2020 at 20:15)</a>:</h4>
<p>I'm familiar with the generalities of electrolysis but not in detail. It uses a rather different translation and representation for borrows though</p>



<a name="209561995"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209561995" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209561995">(Sep 09 2020 at 20:17)</a>:</h4>
<p>it predates the work on RustHorn by several years though</p>



<a name="209562060"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209562060" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209562060">(Sep 09 2020 at 20:17)</a>:</h4>
<p>It does reference RustBelt which was ongoing work at the time and formalized a Rust kernel language (lambda rust)</p>



<a name="209562541"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209562541" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209562541">(Sep 09 2020 at 20:21)</a>:</h4>
<p>In electrolysis borrows are represented by lenses into a structure  whereas the key detail of both our and RustHorn's approach is to represent mutable borrows as a pair of a current and final value</p>



<a name="209760340"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209760340" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209760340">(Sep 11 2020 at 09:47)</a>:</h4>
<p><span class="user-mention" data-user-id="312719">@Xavier Denis</span> nice work :) the RustHorn idea is ingenious, and I am very curious what will come out of that.</p>



<a name="209760546"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209760546" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209760546">(Sep 11 2020 at 09:48)</a>:</h4>
<p>One thing I am wondering -- you write that it is crucial that you know when a lifetime ends. I do not have a deep understanding of Polonius, but from what I gather, the notion of lifetime there isn't really associated with a region of code any more, so there's no (fixed) "place where a lifetime ends". That is one reason why Stacked Borrows, unlike my earlier approach, does not rely any more on such a place being syntactically fixed. Do you have any thoughts for how to handle that with your approach?</p>



<a name="209869406"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209869406" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209869406">(Sep 12 2020 at 07:39)</a>:</h4>
<p>I mean in polonius the regions (lifetimes) still have a static subgraph they are active over</p>



<a name="209869408"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209869408" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209869408">(Sep 12 2020 at 07:39)</a>:</h4>
<p>I mean in polonius the regions (lifetimes) still have a static subgraph they are active over</p>



<a name="209869409"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209869409" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209869409">(Sep 12 2020 at 07:39)</a>:</h4>
<p>Afaik</p>



<a name="209869453"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209869453" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209869453">(Sep 12 2020 at 07:40)</a>:</h4>
<p>With this approach  we only require that each edge out of that subgraph is a thaw instruction for the associated lifetime</p>



<a name="209869464"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209869464" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209869464">(Sep 12 2020 at 07:41)</a>:</h4>
<p>We absolutely do not require thee to be a unique thaw instruction, so it’s possible to encode NLL programs</p>



<a name="209869469"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209869469" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209869469">(Sep 12 2020 at 07:41)</a>:</h4>
<p>Stacked Borrows is another thing though since we’d need a static over approximation</p>



<a name="209869483"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209869483" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209869483">(Sep 12 2020 at 07:42)</a>:</h4>
<p>Which is something Vytautas is looking at I believe</p>



<a name="209870891"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Master%27s%20Work/near/209870891" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Master&#x27;s.20Work.html#209870891">(Sep 12 2020 at 08:22)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Master's.20Work/near/209869469">said</a>:</p>
<blockquote>
<p>Stacked Borrows is another thing though since we’d need a static over approximation</p>
</blockquote>
<p>that static overapproximation already exists, it is called the borrow checker ;)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>